Notions of computation and monads

Eugenio Moggi, Notions of computation and monads,

Information and Computation, Volume 93, Issue 1, 1991, Pages 55-92, ISSN 0890-5401,

https://doi.org/10.1016/0890-5401(91)90052-4 .

Abstract

The λ-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with λ-terms. However, if one goes further and uses βη-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation.